fischer{$x:ut2, $try:ut2, $taken:ut2, $contending:ut2, $free:ut2, $mine:ut2, $wanted:ut2, $z:ut2}
fischer(es; L)
== e:es-E(es). 
== (loc(e)  L)
==  (es-dtype(es; loc(e); mkid{$x:ut2}; Id)
==  c (((es-after(es; mkid{$x:ut2}; e) = mkid{$free:ut2})
==  c ( (es-after(es; mkid{$x:ut2}; e) = mkid{$taken:ut2})
==  c ( (es-after(es; mkid{$x:ut2}; e) = mkid{$mine:ut2})
==  c ( (es-after(es; mkid{$x:ut2}; e) = mkid{$try:ut2})
==  c ( (es-after(es; mkid{$x:ut2}; e) = mkid{$contending:ut2}))
==  c  (es-initially(es; loc(e); mkid{$x:ut2}) = mkid{$free:ut2})
==  c  (@e(mkid{$x:ut2}mkid{$try:ut2})
==  c   (((es-when(es; mkid{$x:ut2}; e) = mkid{$free:ut2})
==  c    (es-when(es; mkid{$x:ut2}; e) = mkid{$contending:ut2}))
==  c    l_all(L;
==  c    l_all(Id;
==  c    l_all(i.(((i = loc(e)))
==  c    l_all( (e sends on <loc(e), i, mkid{$z:ut2}> with tag mkid{$wanted:ut2})))))
==  c  (@e(mkid{$x:ut2}mkid{$mine:ut2})  (es-when(es; mkid{$x:ut2}; e) = mkid{$try:ut2}))
==  c  (@e(mkid{$x:ut2}mkid{$free:ut2})
==  c   (((es-when(es; mkid{$x:ut2}; e) = mkid{$taken:ut2})
==  c    ((es-isrcv(es; e))
==  c    c ((es-tag(es; e) = mkid{$free:ut2})
==  c    c  (i:Id
==  c    c  (((i  L)
==  c    c  ( ((i = loc(e)))
==  c    c  ( (es-lnk(es; e) = <i, loc(e), mkid{$z:ut2}>))))))
==  c    ((es-when(es; mkid{$x:ut2}; e) = mkid{$mine:ut2})
==  c     l_all(L;
==  c     l_all(Id;
==  c     l_all(i.(((i = loc(e)))
==  c     l_all( (e sends on <loc(e), i, mkid{$z:ut2}> with tag mkid{$free:ut2}))))))
==  c  (@e(mkid{$x:ut2}mkid{$contending:ut2})
==  c   ((es-when(es; mkid{$x:ut2}; e) = mkid{$try:ut2})
==  c    ((es-isrcv(es; e))
==  c    c ((es-tag(es; e) = mkid{$wanted:ut2})
==  c    c  (i:Id
==  c    c  (((i  L)
==  c    c  ( ((i = loc(e)))
==  c    c  ( (es-lnk(es; e) = <i, loc(e), mkid{$z:ut2}>)))))))
==  c  (@e(mkid{$x:ut2}mkid{$taken:ut2})
==  c   (((es-when(es; mkid{$x:ut2}; e) = mkid{$contending:ut2})
==  c    (es-when(es; mkid{$x:ut2}; e) = mkid{$free:ut2}))
==  c    ((es-isrcv(es; e))
==  c    c ((es-tag(es; e) = mkid{$wanted:ut2})
==  c    c  (i:Id
==  c    c  (((i  L)
==  c    c  ( ((i = loc(e)))
==  c    c  ( (es-lnk(es; e) = <i, loc(e), mkid{$z:ut2}>)))))))
==  c  ((es-isrcv(es; e))
==  c   (es-tag(es; e) = mkid{$free:ut2})
==  c   (i:Id. ((i  L)  ((i = loc(e)))  (es-lnk(es; e) = <i, loc(e), mkid{$z:ut2}>)))
==  c   (subtype_rel(es-vartype(es; loc(es-sender(es; e)); mkid{$x:ut2}); Id)
==  c   c (@es-sender(es; e)(mkid{$x:ut2}mkid{$free:ut2})
==  c   c  (es-when(es; mkid{$x:ut2}; es-sender(es; e)) = mkid{$mine:ut2}))))
==  c  ((es-isrcv(es; e))
==  c   (es-tag(es; e) = mkid{$wanted:ut2})
==  c   (i:Id. ((i  L)  ((i = loc(e)))  (es-lnk(es; e) = <i, loc(e), mkid{$z:ut2}>)))
==  c   (subtype_rel(es-vartype(es; loc(es-sender(es; e)); mkid{$x:ut2}); Id)
==  c   c @es-sender(es; e)(mkid{$x:ut2}mkid{$try:ut2}))))) 

latex

---

clarification:

fischer{$x:ut2, $try:ut2, $taken:ut2, $contending:ut2, $free:ut2, $mine:ut2, $wanted:ut2, $z:ut2}
fischer(es; L)
== e:es-E(es). 
== (es-loc(es; e)  L  Id)
==  (es-dtype(es; es-loc(es; e); mkid{$x:ut2}; Id)
==  c (((es-after(es; mkid{$x:ut2}; e) = mkid{$free:ut2}  Id)
==  c ( (es-after(es; mkid{$x:ut2}; e) = mkid{$taken:ut2}  Id)
==  c ( (es-after(es; mkid{$x:ut2}; e) = mkid{$mine:ut2}  Id)
==  c ( (es-after(es; mkid{$x:ut2}; e) = mkid{$try:ut2}  Id)
==  c ( (es-after(es; mkid{$x:ut2}; e) = mkid{$contending:ut2}  Id))
==  c  (es-initially(es; es-loc(es; e); mkid{$x:ut2}) = mkid{$free:ut2}  Id)
==  c  (es-change-to(es;Id;mkid{$x:ut2};e;mkid{$try:ut2})
==  c   (((es-when(es; mkid{$x:ut2}; e) = mkid{$free:ut2}  Id)
==  c    (es-when(es; mkid{$x:ut2}; e) = mkid{$contending:ut2}  Id))
==  c    l_all(L;
==  c    l_all(Id;
==  c    l_all(i.(((i = es-loc(es; e)  Id))
==  c    l_all( es-sends-on(es;e;<es-loc(es; e), i, mkid{$z:ut2}>;mkid{$wanted:ut2})))))
==  c  (es-change-to(es;Id;mkid{$x:ut2};e;mkid{$mine:ut2})
==  c   (es-when(es; mkid{$x:ut2}; e) = mkid{$try:ut2}  Id))
==  c  (es-change-to(es;Id;mkid{$x:ut2};e;mkid{$free:ut2})
==  c   (((es-when(es; mkid{$x:ut2}; e) = mkid{$taken:ut2}  Id)
==  c    ((es-isrcv(es; e))
==  c    c ((es-tag(es; e) = mkid{$free:ut2}  Id)
==  c    c  (i:Id
==  c    c  (((i  L  Id)
==  c    c  ( ((i = es-loc(es; e)  Id))
==  c    c  ( (es-lnk(es; e) = <i, es-loc(es; e), mkid{$z:ut2}>  IdLnk))))))
==  c    ((es-when(es; mkid{$x:ut2}; e) = mkid{$mine:ut2}  Id)
==  c     l_all(L;
==  c     l_all(Id;
==  c     l_all(i.(((i = es-loc(es; e)  Id))
==  c     l_all( es-sends-on(es;e;<es-loc(es; e), i, mkid{$z:ut2}>;mkid{$free:ut2}))))))
==  c  (es-change-to(es;Id;mkid{$x:ut2};e;mkid{$contending:ut2})
==  c   ((es-when(es; mkid{$x:ut2}; e) = mkid{$try:ut2}  Id)
==  c    ((es-isrcv(es; e))
==  c    c ((es-tag(es; e) = mkid{$wanted:ut2}  Id)
==  c    c  (i:Id
==  c    c  (((i  L  Id)
==  c    c  ( ((i = es-loc(es; e)  Id))
==  c    c  ( (es-lnk(es; e) = <i, es-loc(es; e), mkid{$z:ut2}>  IdLnk)))))))
==  c  (es-change-to(es;Id;mkid{$x:ut2};e;mkid{$taken:ut2})
==  c   (((es-when(es; mkid{$x:ut2}; e) = mkid{$contending:ut2}  Id)
==  c    (es-when(es; mkid{$x:ut2}; e) = mkid{$free:ut2}  Id))
==  c    ((es-isrcv(es; e))
==  c    c ((es-tag(es; e) = mkid{$wanted:ut2}  Id)
==  c    c  (i:Id
==  c    c  (((i  L  Id)
==  c    c  ( ((i = es-loc(es; e)  Id))
==  c    c  ( (es-lnk(es; e) = <i, es-loc(es; e), mkid{$z:ut2}>  IdLnk)))))))
==  c  ((es-isrcv(es; e))
==  c   (es-tag(es; e) = mkid{$free:ut2}  Id)
==  c   (i:Id
==  c   (((i  L  Id)
==  c   ( ((i = es-loc(es; e)  Id))
==  c   ( (es-lnk(es; e) = <i, es-loc(es; e), mkid{$z:ut2}>  IdLnk)))
==  c   (subtype_rel(es-vartype(es; es-loc(es; es-sender(es; e)); mkid{$x:ut2}); Id)
==  c   c (es-change-to(es;Id;mkid{$x:ut2};es-sender(es; e);mkid{$free:ut2})
==  c   c  (es-when(es; mkid{$x:ut2}; es-sender(es; e)) = mkid{$mine:ut2}  Id))))
==  c  ((es-isrcv(es; e))
==  c   (es-tag(es; e) = mkid{$wanted:ut2}  Id)
==  c   (i:Id
==  c   (((i  L  Id)
==  c   ( ((i = es-loc(es; e)  Id))
==  c   ( (es-lnk(es; e) = <i, es-loc(es; e), mkid{$z:ut2}>  IdLnk)))
==  c   (subtype_rel(es-vartype(es; es-loc(es; es-sender(es; e)); mkid{$x:ut2}); Id)
==  c   c es-change-to(es;Id;mkid{$x:ut2};es-sender(es; e);mkid{$try:ut2}))))) 

latex

Definitions	x:A. B(x), es-E(es), es-dtype(es; i; x; T), es-after(es; x; e), es-initially(es; i; x), l_all(L; T; x.P(x)), (e sends on l with tag tg), P  Q, P  Q, es-when(es; x; e), b, es-isrcv(es; e), es-tag(es; e), P  Q, x:A. B(x), (x  l), P  Q, A, s = t, IdLnk, es-lnk(es; e), <a, b>, A c B, es-vartype(es; i; x), loc(e), @e(xv), Id, es-sender(es; e), mkid{$x:ut2}
FDL editor aliases	fischer